Inference at * 1 
Iof proof for Lemma ax choice:



1. A : Type
2. B : Type
3. Q : AB
4. x:A. y:B. Q(x,y)
  f:AB. (x:A. Q(x,f(x))) 

latex

 by ((Unfolds ``all exists`` 4) 
CollapseTHEN (RenameVar `g' 4)) 

latex

C1: 

C1: 4. x:Ay:B  Q(x,y)
C1:   f:AB. (x:A. Q(x,f(x)))
C.

Definitions

x:A. B(x), x:A. B(x)